02500	OP
02600	←(V1,A1)
02700	NIL
02800	NIL
02900	NIL
03000	ISVAR(V1);;
03100	C(V1,A1);;
03200	
03300	
03310	ITERATIVE
03320	TUNIFY
03330	NIL
03340	NIL
03350	NIL
03360	NEWVAR(V7);NEWVAR(V8);NEWVAR(V12);NEWVAR(V13);VUNIFY(V4,V5,V6);C(V3,V4);C(V7,V5);C(V8,V6);
03365	  C(V12,V1);C(V13,V2);;
03370	C(V3,V9);C(V7,V10);C(V8,V11);VUNIFY(V9,V10,V11);;
03380	CUNIFY1(V3 V9 (CAR V12)(CAR V13));C(V7, (CONS V7, (CAR V12)));C(V8,(CONS V8, (CAR V13)));
03385	C(V12, (CDR V12));C(V13, (CDR V13));;
03390	=(V12 NIL);;
03400	UNIFY(V3 V1 V2);;
03410	CUNIFY(V3 V1 V2);;
03420	
03430	OP
03440	VARVAR(V3,V9,T1,T2)
03450	NIL
03460	NIL
03470	NIL
03480	VAR(T1);VAR(T2);;
03490	CUNIFY1(V3,V9,T1,T2);C(V3,(CONS(CONS T1,T2),V9));;
03500	AXIOM
03510	TAUNIFY
03520	NIL
03530	T
03540	NIL
03550	=(V9,V9);;
03560	VUNIFY(V9,V10,V11);;
03570	
03700	
04550	NIL
04700	NIL
04800	
04900	ISVAR(Z);VUNIFY(NIL,NIL,NIL);;
05000	
05100	T
05200	
05600	((C T NIL NIL (X,*))
05610	(VAR T T NIL NIL)
05731	(= T NIL NIL NIL)
05733	(CUNIFY T NIL NIL NIL )
05735	(CUNIFY1 T NIL NIL NIL)
05737	(VUNIFY T NIL NIL NIL)
05738	(UNIFY T NIL NIL NIL))
05741	
05760	
06100	
06200	NIL
06300